YES 1.5090000000000001 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ BR

mainModule Main
  ((notElem :: Eq a => Maybe a  ->  [Maybe a ->  Bool) :: Eq a => Maybe a  ->  [Maybe a ->  Bool)

module Main where
  import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ BR
HASKELL
      ↳ COR

mainModule Main
  ((notElem :: Eq a => Maybe a  ->  [Maybe a ->  Bool) :: Eq a => Maybe a  ->  [Maybe a ->  Bool)

module Main where
  import qualified Prelude



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
HASKELL
          ↳ Narrow

mainModule Main
  (notElem :: Eq a => Maybe a  ->  [Maybe a ->  Bool)

module Main where
  import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(xv2000), Succ(xv4001000)) → new_primPlusNat(xv2000, xv4001000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(xv30100), Succ(xv400100)) → new_primMulNat(xv30100, Succ(xv400100))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primEqNat(Succ(xv3000), Succ(xv40000)) → new_primEqNat(xv3000, xv40000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_esEs0(Just(:(xv300, xv301)), Just(:(xv4000, xv4001)), app(ty_[], app(ty_[], bb))) → new_esEs(xv300, xv4000, bb)
new_esEs0(Just(Right(xv300)), Just(Right(xv4000)), app(app(ty_Either, bcb), app(app(ty_@2, bce), bcf))) → new_esEs1(xv300, xv4000, bce, bcf)
new_esEs3(Right(xv300), Right(xv4000), bcb, app(ty_[], bcc)) → new_esEs(xv300, xv4000, bcc)
new_esEs2(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), fa, app(app(ty_Either, he), hf), gf) → new_esEs3(xv301, xv4001, he, hf)
new_esEs0(Just(@3(xv300, xv301, xv302)), Just(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, fa), app(ty_[], ge)), gf)) → new_esEs(xv301, xv4001, ge)
new_esEs2(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), fa, fb, app(app(ty_@2, ff), fg)) → new_esEs1(xv302, xv4002, ff, fg)
new_esEs0(Just(Left(xv300)), Just(Left(xv4000)), app(app(ty_Either, app(ty_Maybe, bbb)), bba)) → new_esEs0(xv300, xv4000, bbb)
new_esEs0(Just(:(xv300, xv301)), Just(:(xv4000, xv4001)), app(ty_[], ba)) → new_esEs(xv301, xv4001, ba)
new_esEs1(@2(xv300, xv301), @2(xv4000, xv4001), cd, app(app(app(ty_@3, db), dc), dd)) → new_esEs2(xv301, xv4001, db, dc, dd)
new_esEs0(Just(Left(xv300)), Just(Left(xv4000)), app(app(ty_Either, app(app(ty_Either, bbh), bca)), bba)) → new_esEs3(xv300, xv4000, bbh, bca)
new_esEs3(Right(xv300), Right(xv4000), bcb, app(app(ty_Either, bdb), bdc)) → new_esEs3(xv300, xv4000, bdb, bdc)
new_esEs2(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(ty_[], hg), fb, gf) → new_esEs(xv300, xv4000, hg)
new_esEs0(Just(@3(xv300, xv301, xv302)), Just(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, app(ty_Maybe, hh)), fb), gf)) → new_esEs0(xv300, xv4000, hh)
new_esEs0(Just(xv30), Just(xv400), app(ty_Maybe, cc)) → new_esEs0(xv30, xv400, cc)
new_esEs0(Just(:(xv300, xv301)), Just(:(xv4000, xv4001)), app(ty_[], app(app(ty_@2, bd), be))) → new_esEs1(xv300, xv4000, bd, be)
new_esEs0(Just(Right(xv300)), Just(Right(xv4000)), app(app(ty_Either, bcb), app(ty_Maybe, bcd))) → new_esEs0(xv300, xv4000, bcd)
new_esEs0(Just(@3(xv300, xv301, xv302)), Just(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, app(app(ty_Either, baf), bag)), fb), gf)) → new_esEs3(xv300, xv4000, baf, bag)
new_esEs3(Left(xv300), Left(xv4000), app(app(ty_Either, bbh), bca), bba) → new_esEs3(xv300, xv4000, bbh, bca)
new_esEs0(Just(:(xv300, xv301)), Just(:(xv4000, xv4001)), app(ty_[], app(app(app(ty_@3, bf), bg), bh))) → new_esEs2(xv300, xv4000, bf, bg, bh)
new_esEs2(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), fa, fb, app(ty_Maybe, fd)) → new_esEs0(xv302, xv4002, fd)
new_esEs0(Just(Right(xv300)), Just(Right(xv4000)), app(app(ty_Either, bcb), app(app(app(ty_@3, bcg), bch), bda))) → new_esEs2(xv300, xv4000, bcg, bch, bda)
new_esEs0(Just(@3(xv300, xv301, xv302)), Just(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, app(app(app(ty_@3, bac), bad), bae)), fb), gf)) → new_esEs2(xv300, xv4000, bac, bad, bae)
new_esEs0(Just(@2(xv300, xv301)), Just(@2(xv4000, xv4001)), app(app(ty_@2, cd), app(app(ty_@2, cg), da))) → new_esEs1(xv301, xv4001, cg, da)
new_esEs0(Just(:(xv300, xv301)), Just(:(xv4000, xv4001)), app(ty_[], app(ty_Maybe, bc))) → new_esEs0(xv300, xv4000, bc)
new_esEs2(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(app(ty_@2, baa), bab), fb, gf) → new_esEs1(xv300, xv4000, baa, bab)
new_esEs1(@2(xv300, xv301), @2(xv4000, xv4001), cd, app(app(ty_Either, de), df)) → new_esEs3(xv301, xv4001, de, df)
new_esEs(:(xv300, xv301), :(xv4000, xv4001), app(ty_Maybe, bc)) → new_esEs0(xv300, xv4000, bc)
new_esEs1(@2(xv300, xv301), @2(xv4000, xv4001), cd, app(app(ty_@2, cg), da)) → new_esEs1(xv301, xv4001, cg, da)
new_esEs0(Just(@2(xv300, xv301)), Just(@2(xv4000, xv4001)), app(app(ty_@2, app(ty_Maybe, ea)), dh)) → new_esEs0(xv300, xv4000, ea)
new_esEs(:(xv300, xv301), :(xv4000, xv4001), app(app(ty_Either, ca), cb)) → new_esEs3(xv300, xv4000, ca, cb)
new_esEs0(Just(@2(xv300, xv301)), Just(@2(xv4000, xv4001)), app(app(ty_@2, app(ty_[], dg)), dh)) → new_esEs(xv300, xv4000, dg)
new_esEs0(Just(Right(xv300)), Just(Right(xv4000)), app(app(ty_Either, bcb), app(app(ty_Either, bdb), bdc))) → new_esEs3(xv300, xv4000, bdb, bdc)
new_esEs2(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), fa, app(app(ty_@2, gh), ha), gf) → new_esEs1(xv301, xv4001, gh, ha)
new_esEs0(Just(@2(xv300, xv301)), Just(@2(xv4000, xv4001)), app(app(ty_@2, cd), app(ty_[], ce))) → new_esEs(xv301, xv4001, ce)
new_esEs0(Just(@3(xv300, xv301, xv302)), Just(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, app(ty_[], hg)), fb), gf)) → new_esEs(xv300, xv4000, hg)
new_esEs1(@2(xv300, xv301), @2(xv4000, xv4001), app(app(ty_Either, eg), eh), dh) → new_esEs3(xv300, xv4000, eg, eh)
new_esEs0(Just(@2(xv300, xv301)), Just(@2(xv4000, xv4001)), app(app(ty_@2, app(app(app(ty_@3, ed), ee), ef)), dh)) → new_esEs2(xv300, xv4000, ed, ee, ef)
new_esEs0(Just(@3(xv300, xv301, xv302)), Just(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, fa), fb), app(ty_Maybe, fd))) → new_esEs0(xv302, xv4002, fd)
new_esEs3(Right(xv300), Right(xv4000), bcb, app(ty_Maybe, bcd)) → new_esEs0(xv300, xv4000, bcd)
new_esEs3(Left(xv300), Left(xv4000), app(ty_Maybe, bbb), bba) → new_esEs0(xv300, xv4000, bbb)
new_esEs2(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), fa, fb, app(app(app(ty_@3, fh), ga), gb)) → new_esEs2(xv302, xv4002, fh, ga, gb)
new_esEs1(@2(xv300, xv301), @2(xv4000, xv4001), app(ty_Maybe, ea), dh) → new_esEs0(xv300, xv4000, ea)
new_esEs2(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(app(app(ty_@3, bac), bad), bae), fb, gf) → new_esEs2(xv300, xv4000, bac, bad, bae)
new_esEs0(Just(@3(xv300, xv301, xv302)), Just(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, fa), app(app(app(ty_@3, hb), hc), hd)), gf)) → new_esEs2(xv301, xv4001, hb, hc, hd)
new_esEs2(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), fa, fb, app(ty_[], fc)) → new_esEs(xv302, xv4002, fc)
new_esEs0(Just(@3(xv300, xv301, xv302)), Just(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, fa), app(app(ty_Either, he), hf)), gf)) → new_esEs3(xv301, xv4001, he, hf)
new_esEs0(Just(Left(xv300)), Just(Left(xv4000)), app(app(ty_Either, app(app(ty_@2, bbc), bbd)), bba)) → new_esEs1(xv300, xv4000, bbc, bbd)
new_esEs0(Just(Right(xv300)), Just(Right(xv4000)), app(app(ty_Either, bcb), app(ty_[], bcc))) → new_esEs(xv300, xv4000, bcc)
new_esEs0(Just(@2(xv300, xv301)), Just(@2(xv4000, xv4001)), app(app(ty_@2, app(app(ty_@2, eb), ec)), dh)) → new_esEs1(xv300, xv4000, eb, ec)
new_esEs(:(xv300, xv301), :(xv4000, xv4001), app(app(app(ty_@3, bf), bg), bh)) → new_esEs2(xv300, xv4000, bf, bg, bh)
new_esEs2(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), fa, app(ty_Maybe, gg), gf) → new_esEs0(xv301, xv4001, gg)
new_esEs0(Just(Left(xv300)), Just(Left(xv4000)), app(app(ty_Either, app(ty_[], bah)), bba)) → new_esEs(xv300, xv4000, bah)
new_esEs0(Just(@3(xv300, xv301, xv302)), Just(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, app(app(ty_@2, baa), bab)), fb), gf)) → new_esEs1(xv300, xv4000, baa, bab)
new_esEs3(Left(xv300), Left(xv4000), app(ty_[], bah), bba) → new_esEs(xv300, xv4000, bah)
new_esEs0(Just(@3(xv300, xv301, xv302)), Just(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, fa), fb), app(app(app(ty_@3, fh), ga), gb))) → new_esEs2(xv302, xv4002, fh, ga, gb)
new_esEs1(@2(xv300, xv301), @2(xv4000, xv4001), cd, app(ty_[], ce)) → new_esEs(xv301, xv4001, ce)
new_esEs2(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(ty_Maybe, hh), fb, gf) → new_esEs0(xv300, xv4000, hh)
new_esEs0(Just(@2(xv300, xv301)), Just(@2(xv4000, xv4001)), app(app(ty_@2, app(app(ty_Either, eg), eh)), dh)) → new_esEs3(xv300, xv4000, eg, eh)
new_esEs1(@2(xv300, xv301), @2(xv4000, xv4001), app(ty_[], dg), dh) → new_esEs(xv300, xv4000, dg)
new_esEs(:(xv300, xv301), :(xv4000, xv4001), app(app(ty_@2, bd), be)) → new_esEs1(xv300, xv4000, bd, be)
new_esEs(:(xv300, xv301), :(xv4000, xv4001), ba) → new_esEs(xv301, xv4001, ba)
new_esEs0(Just(@3(xv300, xv301, xv302)), Just(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, fa), fb), app(app(ty_Either, gc), gd))) → new_esEs3(xv302, xv4002, gc, gd)
new_esEs2(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(app(ty_Either, baf), bag), fb, gf) → new_esEs3(xv300, xv4000, baf, bag)
new_esEs3(Left(xv300), Left(xv4000), app(app(ty_@2, bbc), bbd), bba) → new_esEs1(xv300, xv4000, bbc, bbd)
new_esEs2(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), fa, app(app(app(ty_@3, hb), hc), hd), gf) → new_esEs2(xv301, xv4001, hb, hc, hd)
new_esEs1(@2(xv300, xv301), @2(xv4000, xv4001), app(app(ty_@2, eb), ec), dh) → new_esEs1(xv300, xv4000, eb, ec)
new_esEs0(Just(@2(xv300, xv301)), Just(@2(xv4000, xv4001)), app(app(ty_@2, cd), app(ty_Maybe, cf))) → new_esEs0(xv301, xv4001, cf)
new_esEs2(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), fa, app(ty_[], ge), gf) → new_esEs(xv301, xv4001, ge)
new_esEs3(Right(xv300), Right(xv4000), bcb, app(app(app(ty_@3, bcg), bch), bda)) → new_esEs2(xv300, xv4000, bcg, bch, bda)
new_esEs0(Just(@3(xv300, xv301, xv302)), Just(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, fa), app(ty_Maybe, gg)), gf)) → new_esEs0(xv301, xv4001, gg)
new_esEs0(Just(@2(xv300, xv301)), Just(@2(xv4000, xv4001)), app(app(ty_@2, cd), app(app(app(ty_@3, db), dc), dd))) → new_esEs2(xv301, xv4001, db, dc, dd)
new_esEs0(Just(@3(xv300, xv301, xv302)), Just(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, fa), fb), app(app(ty_@2, ff), fg))) → new_esEs1(xv302, xv4002, ff, fg)
new_esEs0(Just(@3(xv300, xv301, xv302)), Just(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, fa), fb), app(ty_[], fc))) → new_esEs(xv302, xv4002, fc)
new_esEs0(Just(Left(xv300)), Just(Left(xv4000)), app(app(ty_Either, app(app(app(ty_@3, bbe), bbf), bbg)), bba)) → new_esEs2(xv300, xv4000, bbe, bbf, bbg)
new_esEs3(Left(xv300), Left(xv4000), app(app(app(ty_@3, bbe), bbf), bbg), bba) → new_esEs2(xv300, xv4000, bbe, bbf, bbg)
new_esEs2(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), fa, fb, app(app(ty_Either, gc), gd)) → new_esEs3(xv302, xv4002, gc, gd)
new_esEs3(Right(xv300), Right(xv4000), bcb, app(app(ty_@2, bce), bcf)) → new_esEs1(xv300, xv4000, bce, bcf)
new_esEs1(@2(xv300, xv301), @2(xv4000, xv4001), cd, app(ty_Maybe, cf)) → new_esEs0(xv301, xv4001, cf)
new_esEs0(Just(:(xv300, xv301)), Just(:(xv4000, xv4001)), app(ty_[], app(app(ty_Either, ca), cb))) → new_esEs3(xv300, xv4000, ca, cb)
new_esEs(:(xv300, xv301), :(xv4000, xv4001), app(ty_[], bb)) → new_esEs(xv300, xv4000, bb)
new_esEs0(Just(@2(xv300, xv301)), Just(@2(xv4000, xv4001)), app(app(ty_@2, cd), app(app(ty_Either, de), df))) → new_esEs3(xv301, xv4001, de, df)
new_esEs0(Just(@3(xv300, xv301, xv302)), Just(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, fa), app(app(ty_@2, gh), ha)), gf)) → new_esEs1(xv301, xv4001, gh, ha)
new_esEs1(@2(xv300, xv301), @2(xv4000, xv4001), app(app(app(ty_@3, ed), ee), ef), dh) → new_esEs2(xv300, xv4000, ed, ee, ef)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_foldr(xv3, :(xv40, xv41), ba) → new_foldr(xv3, xv41, ba)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: